$\forall$${\it es}$:ES, $P$, $Q$:(E$\rightarrow\mathbb{P}$), $T$, ${\it T'}$:Type, $R$:($T$$\rightarrow$${\it T'}$$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$e$:E. $P$($e$) $\Rightarrow$ (valtype($e$) $\subseteq$r $T$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. $Q$($e$) $\Rightarrow$ (valtype($e$) $\subseteq$r ${\it T'}$))
\\[0ex]$\Rightarrow$ (($e$.$P$($e$) $\rightarrow\rightarrow$ $e$.$Q$($e$)) with $R$ $\in$ $\mathbb{P}$)